Nuprl Lemma : normalize-constraints-eq
11,40
postcript
pdf
k
:
,
A
:((
:(
)
) List). normalize-constraints(
k
;
A
) =
A
latex
Definitions
has-value(
a
)
,
Y
,
P
Q
,
map(
f
;
as
)
,
map-eval(
x
.
f
(
x
);
L
)
,
normalize-constraints(
k
;
A
)
,
t
T
,
x
:
A
.
B
(
x
)
,
Lemmas
normalize-constraint-eq
,
l
member
wf
,
trivial
map
,
normalize-constraint
wf
,
rationals
wf
,
nat
wf
origin
k:
, A:((:(
) 
) List). normalize-constraints(k;A) = A k:, A:((:() ) List). normalize-constraints(k;A) = A 
Q
Tx:A. B(x)